| Definitions | (last change to x before e), @e(x v),  e (e1,e2].P(e), x(s), filter(P;l), SQType(T), l[i], ||as||, Y, P  Q, f  g, IsPrimeIdeal(R;P), IsIntegDom(r), a  b, IsMonHom{M1,M2}(f), IsGroup(T;op;id;inv), IsMonoid(T;op;id), monot(T;x,y.R(x;y);f), Cancel(T;S;op), FunThru2op(A;B;opa;opb;f), fun_thru_1op(A;B;opa;opb;f), Dist1op2opLR(A;1op;2op), IsAction(A;x;e;S;f), IsBilinear(A;B;C;+a;+b;+c;f), BiLinear(T;pl;tm), Inverse(T;op;id;inv), Comm(T;op), Assoc(T;op), Ident(T;op;id), CoPrime(a,b), Connex(T;x,y.R(x;y)), AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), IsEqFun(T;eq), Inj(A;B;f), InvFuns(A;B;f;g), a =!x:T. Q(x), SqStable(P),  e(e1,e2].P(e), e[e1,e2].P(e), e[e1,e2].P(e), e[e1,e2).P(e), e[e1,e2).P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e<e'.P(e), l_disjoint(T;l1;l2), q-rel(r;x), r < s, y is f*(x), (xL.P(x)), xL. P(x), A c B, a < b, a <p b, a b, a ~ b, b | a, Dec(P), e c e', e loc e' , map(f;as), x dom(f),  T, inl x , inr x , True, s ~ t, A List , before(e), pred(e), case b of inl(x) => s(x) | inr(y) => t(y), (e <loc e'), loc(e), mapfilter(f;P;L), first(e), -n, i  j ,  x.A(x), pred(e), first(e), suptype(S; T), pred!(e;e'), kind(e), loc(e), SWellFounded(R(x;y)), x:A. B(x), (x l), |g|, n - m, S T, n+m, #$n, Outcome, A B, False, {T}, a < b, constant_function(f;A;B), r s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time),  ,  , Msg(M), kindcase(k; a.f(a); l,t.g(l;t) ),  x,y. t(x;y), x. t(x), Knd, EState(T), EOrderAxioms(E; pred?; info), Id, IdLnk, EqDecider(T), Unit,  , p  q, p q, p   q, e = e', deq-member(eq;x;L), a = b, a = b, qeq(r;s), q_less(a;b), q_le(r;s), eq_atom$n(x;y), [d], a < b, x f y, f(a), a < b, null(as), x =a y, (i = j), i z j, i <z j, p =b q, E(X), a:A fp B(a), strong-subtype(A;B), f(x)?z, P  Q, P & Q, P Q, {x:A| B(x)} ,  x:A.B(x), Void, Top, tt,  b, (e < e'), if b then t else f fi , as @ bs, es-prior-interface-vals(es;X;e), [car / cdr], X(e), [], t.1, let x,y = A in B(x;y), left + right, x:A  B(x), P Q, type List, <a, b>,  ,  , e X, prior(X), ff, E, AbsInterface(A), Type, ES, A,  b, x:A. B(x), x:A B(x), s = t, t T |
| Lemmas | assert wf, not wf, bnot wf, bool wf, subtype rel wf, top wf, es-interface-subtype rel, es-interface wf, member wf, es-prior-interface wf, es-E-interface wf, es-E wf, es-is-interface wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, event system wf, deq wf, unit wf, IdLnk wf, Id wf, EOrderAxioms wf, EState wf, Knd wf, kindcase wf, Msg wf, nat wf, rationals wf, val-axiom wf, cless wf, qle wf, constant function wf, false wf, le wf, es-causl wf, guard wf, nat ind tp, es-causl-swellfnd, strongwellfounded wf, pred! wf, first wf, loc wf, kind wf, nat properties, ge wf, es-first wf, append wf, es-interface-val wf, es-is-prior-interface, es-first-implies, es-pred wf, es-before wf, l member wf, mapfilter-append, es-prior-interface-val-pred, rev implies wf, iff wf, bfalse wf, btrue wf, true wf, squash wf, es-interface-val wf2, es-prior-interface-vals wf, append-nil, ifthenelse wf, es-pred-causl, es-E-interface-subtype rel, decidable assert, sq stable from decidable, es-is-prior-interface-pred, length wf nat, filter is nil, es-loc wf, es-locl wf, l all wf, member-es-before |